\documentclass[11pt]{article}
\usepackage[T1]{fontenc}
\usepackage{verbatim}
\usepackage{url}
\usepackage{listings}
\usepackage{graphicx}
\usepackage[left=20mm, right=20mm, top=20mm, bottom=20mm]{geometry}

%
% Clafer code listings
%
\lstdefinelanguage{Clafer}
{morekeywords={abstract, else, in, no, opt, xor, all, enum, lone, not, or, disj, extends, mux, one, some},
sensitive=true,
morecomment=[l][\footnotesize\itshape]{--},
morecomment=[s][\small\itshape]{{-}{-}},
%basicstyle=\footnotesize,
tabsize=4,
columns=fullflexible,
literate={->}{{$\to$ }}1 {^}{{$\mspace{-3mu}\widehat{\quad}\mspace{-3mu}$}}1
 {<}{$<$ }2 {>}{$>$ }2 {>=}{$\geq$ }2 {=<}{$\leq$ }2
 {<:}{{$<\mspace{-3mu}:$}}2 {:>}{{$:\mspace{-3mu}>$}}2
 {=>}{{$\Rightarrow$ }}2 {+}{$+$ }2 {++}{{$+\mspace{-8mu}+$ }}2
 {\~}{{$\mspace{-3mu}\widetilde{\quad}\mspace{-3mu}$}}1
 {!=}{$\neq$ }2 {*}{${}^{\ast}$}1
 {\#}{$\#$}1
 {\`}{\textbf{\`}}1
 {+}{$+$ }1
}

\lstset{basicstyle=\small,language=Clafer,numbers=left,numberstyle={\tiny}}

\newcommand{\figref}[1]{Fig.\,\ref{fig:#1}}
\newcommand{\Figref}[1]{Figure\,\ref{fig:#1}}

\newcommand{\aClass}[1]{\emph{\textsf{#1}}}
\newcommand{\class}[1]{\textsf{#1}}
\newcommand{\property}[1]{\textsf{#1}}
\newcommand{\relationship}[1]{\emph{#1}}

\begin{document}
\title{Clafer Documentation}
\author{Kacper Bak}

\maketitle

\section{Introduction}

This document documents the Clafer language. At present it explains abstract syntax of Clafer related to EMOF and specified in Clafer. The document will be developed incrementally.

% what is clafer? feature modeling, cross tree constraints, general modeling language, class modeling
%\subsection{Why Another Language?}
%\subsection{What Can I Do with Clafer?} % what it is good for

%syntax and grammar (separate file?)
%features, hierarchy, attributes, constraints

%name scope name resolution

%the core language

%\section{Constructions}

%\subsection{Comments}

%\subsection{Features}
%boolean, groups Cardinalities, hierarchy (whitespace, braces), different types of groups, default params
% children, parent

%\subsection{Singletons}

%\subsection{Abstract Features}

%\subsection{Inline Definition and Use}

%\subsection{Abstract Feature Definition and Use}

%\subsection{Inheritance}
%quotation
%default superfeature

%\subsection{Feature-Typed Attribute}

%\subsection{Navigation}

%\subsection{Enumerations}

%\subsection{Constraints}
%logical operators, quantifiers, set operators, arithmetic expressions, strings
%assigning values

%\section{Applications}
%class and fm: mixing, specializing, coupling
% metamodeling
% example from paper
% formal grammars
% logical problems
% model views

%clafer2alloy translator - semantics
%\subsection{Limitations}
% name resolution
% no modules
% no '_' in names allowed
% no overriding

%\subsection{FAQ}
% implied complex constraints - under a feature;
% when to use ref and when inheritance
% how to easilly write implication (constraint under feature or {[feat]}
% aggregation by type (group constraints)

\section{Abstract Syntax (Meta-Model)}

\subsection{Clafer vs EMOF}
\Figref{clafermm} explains the meaning of Clafer with respect to EMOF meta-model. There are two main elements in EMOF: \aClass{Class} and \aClass{Property}. \aClass{NamedElement} is a superclass of both elements. Instances of named elements have an explicit name (e.g. as in Java \textsf{\textbf{class} Object}). The \relationship{superClass} relationship from \aClass{Class} to itself communicates that each \aClass{Class} can have multiple superclasses. The \property{isAbstract} flag makes the \aClass{Class} either abstract or concrete. An abstract class cannot be instantiated unless extended by a concrete class. \aClass{Class} is a subclass of \aClass{Type}, thus declaration of a new \aClass{Class} creates new type. EMOF meta-models' nesting hierarchy is established by the \relationship{ownedAttribute} relationship, i.e. \aClass{Class} contains \aClass{Properties}. Backwards navigation (from \aClass{Property} to its owner) is named \relationship{class}. The \aClass{Property} class is a slot that contains class instances or references to class instances (controlled by the \property{isComposite} flag).

EMOF properties and types are two separate elements. Clafer unifies feature with meta-modeling by introducing the \class{clafer} class that is a subclass of \aClass{Class} and \aClass{Property}. We equate \aClass{Property} with feature from feature modeling. Thus, a feature is also a slot (mathematically, it can be thought of as a binary relation between classes). Single \class{clafer} declaration in Clafer model, creates a new type (class) and also a slot (feature); both of the same name. Such clafers are called containment clafers. Abstract clafers, on the other hand, only declare a new type, and are meant for reuse. Finally, references in Clafer models, do not create new type, but point to existing elements. Their \property{isComposite} flag is set to \textsf{false}. Each \class{clafer} has two types of cardinalities: feature (inherited from \aClass{Property} and group cardinality (contained). The former restricts the number of \class{clafer} instances; the later restricts the number of children instances. Group cardinality applies to the total number of instances stored by children features. Similarly to EMOF, the \relationship{ownedAttribute} makes up the nesting hierarchy.

Having single \class{clafer} class makes the Clafer notation concise and gives it feature modeling flavor. Obviously, the idea might seem at least controversial to some people, but we find found it very convenient in modeling. Clarity and simplicity are one of the biggest advantages of FODA feature models. Clafer was significantly influenced by research on feature models.

\begin{figure}[t]
\begin{center}
\includegraphics[width=0.8\textwidth]{figs/clafermm}
\end{center}%
\vspace{-5mm}%
\caption{\label{fig:clafermm}Clafer's meta-model related to EMOF}
\end{figure}

\subsection{Clafer in Clafer}

\lstset{firstnumber=last}

\subsubsection{Module}
Clafer model is composed of \emph{modules}. Each module introduces a new namespace and contains arbitrary number of \emph{elements}. The purpose of a module is to organize elements into logically-related entities.

\lstinputlisting[firstline=1,lastline=2]{clafermm.cfr}

\subsubsection{Element}
\emph{Element} is a base concept for \emph{clafers} and \emph{constraints}. It is defined as an abstract concept because Clafer models are tree-like recursive structures. Therefore, the element concept is used both in module and clafer definitions. An element has the \emph{Essential} flag, which states whether the element must be present in a valid model or not.

\lstinputlisting[firstline=4,lastline=5]{clafermm.cfr}

\subsubsection{Clafer}
\emph{Clafer} is the very central idea of Clafer language. It unifies types and instances (or classes and objects). It may sound ridiculous at first, but we found that unification allows for more concise models, and naturally fits into relational logic semantics that found its place in formal model analysis and model checking.

A clafer has a \emph{name} specified as a string. Furthermore, it has an optional \emph{super} reference that points to base clafer and establishes inheritance hierarchy. Although most clafers will have super clafers, some of them will not, e.g. reference clafers.

Hierarchical structure is established by recursive nesting of clafers. A clafer can have arbitrary number of \emph{children}, which are either constraints or sub-clafers. If a clafer has sub-clafers, then every child has a \emph{parent} reference pointing to its owner. The reference is optional because top-level clafers have no owners. The optional \emph{reference} clafer points to a set of clafers defined by given set expression. Each clafer has a \emph{groupCardinality} associated with it. It restricts the number of children instances. Finally, optional \emph{cardinalitiy} restricts the number of clafer instances. Both cardinalities are intervals, therefore one can restrict the lower and the higher endpoint.

Clafers are slots that can contain one or more instances or references to instances. Mathematically, clafers are binary relations. There are three types of clafers: abstract clafers, containment clafers, and reference clafers.

\lstinputlisting[firstline=7,lastline=14]{clafermm.cfr}

\subsubsection{Abstract Clafer}
Abstract clafers define a new type (class). They are not instantiated unless extended by a containment clafer. Abstract clafers have no parents because they are always defined at the top level. Furthermore, there are no cardinalities attached to them.

\lstinputlisting[firstline=16,lastline=17]{clafermm.cfr}

\subsubsection{Containment Clafer}
Containment clafers  define a new type and contain instances at the same time. They always have cardinalities that determine the number of clafer instances. Containment clafers usually have children, and sometimes reference other clafers. Clafers with no \emph{children} and \emph{reference} are considered containment clafers.

\lstinputlisting[firstline=19,lastline=20]{clafermm.cfr}

\subsubsection{Reference Clafer}
Reference clafers hold references to instances. They do not create new clafer instances, but point to existing ones. A reference clafer has no children, no parent and no base clafer.

\lstinputlisting[firstline=22,lastline=23]{clafermm.cfr}

\subsubsection{Interval}
Clafer and group cardinalities (\emph{cardinality} and \emph{groupCardinality}, respectively) are intervals determined by two endpoints \emph{min} and \emph{max}. The second one is never smaller than the first one. Maximum can be either a natural number $-1$, which means \emph{unlimited}.

\lstinputlisting[firstline=25,lastline=28]{clafermm.cfr}

\subsubsection{Primitive Clafers}
There are two primitive types wrapped as clafers: \emph{String} and \emph{Integer}. They are no different from \emph{ContainmentClafers}, but they have the \emph{value} child that stores the primitive value.

\lstinputlisting[firstline=30,lastline=34]{clafermm.cfr}

\subsubsection{Constraint}
\emph{Constraints} are a substantial part of the language. At the top level they are \emph{LogicalExpressions} evaluated by reasoning engine. A logical expression can have local variables (\emph{Binding}) and must be one of allowed expressions. An \emph{Expression} is either recursively composed of logical expressions (\emph{MultLogicalExpression}), or relates two expressions (\emph{RelationExpression}), or is a set expression preceded by mandatory quantifier (\emph{QuantifiedSetExpression}).

\lstinputlisting[firstline=36,lastline=45]{clafermm.cfr}

\subsubsection{Quantifiers}
There are four basic quantifiers used for constraining sets. \emph{No} requires the set to be empty, \emph{Lone} requires the set to be empty or a singleton, \emph{One} requires the set to be a singleton, \emph{Some} requires the set to have at least one element.

\lstinputlisting[firstline=47,lastline=52]{clafermm.cfr}

\subsubsection{Binding}
Binding introduces local names for a set expression (\emph{sexp}). The \emph{name} can be used within local logical expression. To say whether the logical expression holds for all or some elements, one uses \emph{Quantifier} extended with \emph{All} (must hold for all elements). The \emph{Disjoint} flag indicates if elements of different names must have different values.

\lstinputlisting[firstline=54,lastline=60]{clafermm.cfr}

\subsubsection{Recursive Logical Expressions}
They are part of \emph{LogicalExpressions}. Recursive logical expressions are composed of logical expressions connected by one of \emph{LogicalOperators}. The \emph{ImpliesElse} operator is equivalent to \emph{if-then-else} statement in programming languages and required 3 arguments. Negation (\emph{Neg}) is a one-argument operator; all other operators act on 2 arguments.

\lstinputlisting[firstline=62,lastline=69]{clafermm.cfr}

\subsubsection{Relation Expression}
It relates two elements, either by comparing elements or stating whether element belongs to a set (\emph{In} and \emph{NIn}); the result is always a Boolean value. Relation expression can refer to two set expressions (\emph{sexp}), or arithmetic expressions (\emph{aexp}), or string expressions (\emph{strexp}).

\lstinputlisting[firstline=71,lastline=80]{clafermm.cfr}

\subsubsection{Quantified Set Expression}
It is a set expression preceded by a \emph{Quantifier}. Application of a quantifier transforms a set expression to a logical expression.

\lstinputlisting[firstline=82,lastline=85]{clafermm.cfr}

\subsubsection{Set Expression}
Set expressions are either a \emph{clafer} or recursive set expressions (\emph{sexp}) joined by set operators.

\lstinputlisting[firstline=87,lastline=95]{clafermm.cfr}

\subsubsection{Arithmetic Expression}
Arithmetic expressions are composed of either \emph{integer} or recursive arithmetic expressions. Unary negation (\emph{UnaryMinus}) and set cardinality (\emph{SetCadinality}) operators take only 1 argument; other operators take 2 arguments.

\lstinputlisting[firstline=97]{clafermm.cfr}




\bibliographystyle{plain}
\nocite{*}
\bibliography{doc}

\end{document}
